home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / lisp / eulisp / mpfeel.lha / MPFeel / Modules / boyer-par-c.em < prev    next >
Lisp/Scheme  |  1992-10-06  |  15KB  |  593 lines
  1. ;; $aclHeader: boyer.cl,v 1.3 90/10/16 11:59:14 layer Rel $
  2.  
  3. ;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
  4. ;;; Fairly CONS intensive.
  5.  
  6. (defmodule boyer-par-c
  7.   (standard0
  8.    plists)
  9.   ()
  10.  
  11.   (defun add-lemma (term)
  12.     (cond ((and (not (atom term))
  13.         (eq (car term)
  14.             (quote equal))
  15.         (not (atom (cadr term))))
  16.        ((setter get) (caadr term) (quote lemmas)
  17.         (cons term (get (caadr term) (quote lemmas)))))
  18.       (t (error "~%ADD-LEMMA did not like term:  ~a" term))))
  19.  
  20.   (defun add-lemma-lst (lst)
  21.     (cond ((null lst)
  22.        t)
  23.       (t (add-lemma (car lst))
  24.          (add-lemma-lst (cdr lst)))))
  25.  
  26.   (defun apply-subst (alist term)
  27.     (let ((**temp-temp** nil))
  28.       (cond ((atom term)
  29.          (cond ((setq **temp-temp** (assoc term alist eq))
  30.             (cdr **temp-temp**))
  31.            (t term)))
  32.         (t (cons (car term)
  33.              (apply-subst-lst alist (cdr term)))))))
  34.  
  35.   (defun apply-subst-lst (alist lst)
  36.     (cond ((null lst)
  37.        nil)
  38.       (t (cons (apply-subst alist (car lst))
  39.            (apply-subst-lst alist (cdr lst))))))
  40.  
  41.   (defun falsep (x lst)
  42.     (or (equal x (quote (f)))
  43.     (member x lst eq)))
  44.  
  45.   (defun one-way-unify (term1 term2 **unify-subst**)
  46.     (progn ((setter car) **unify-subst** nil)
  47.        (one-way-unify1 term1 term2 **unify-subst**)))
  48.  
  49.   (defun one-way-unify1 (term1 term2 **unify-subst**)
  50.     (let ((**temp-temp** nil))
  51.       (cond ((atom term2)
  52.          (cond ((setq **temp-temp** (assoc term2 (car **unify-subst**) eq))
  53.             (equal term1 (cdr **temp-temp**)))
  54.            (t ((setter car) **unify-subst** (cons (cons term2 term1)
  55.                             (car **unify-subst**)))
  56.               t)))
  57.         ((atom term1)
  58.          nil)
  59.         ((eq (car term1)
  60.          (car term2))
  61.          (one-way-unify1-&lst (cdr term1)
  62.                   (cdr term2) **unify-subst**))
  63.         (t nil))))
  64.  
  65.   (defun one-way-unify1-&lst (lst1 lst2 **unify-subst**)
  66.     (cond ((null lst1)
  67.        t)
  68.       ((one-way-unify1 (car lst1)
  69.                (car lst2)
  70.                            **unify-subst**)
  71.        (one-way-unify1-&lst (cdr lst1)
  72.                 (cdr lst2) **unify-subst**))
  73.       (t nil)))
  74.  
  75.   (defun rewrite (term)
  76.     (cond ((atom term)
  77.        term)
  78.       (t (rewrite-with-lemmas (cons (car term)
  79.                     (rewrite-args (cdr term)))
  80.                   (get (car term)
  81.                        (quote lemmas))))))
  82.  
  83.   (defun rewrite-args (lst)
  84.     (cond ((null lst)
  85.        nil)
  86.       (t (cons (rewrite (car lst))
  87.            (rewrite-args (cdr lst))))))
  88.  
  89.   (defun rewrite-with-lemmas (term lst)
  90.     (let ((**unify-subst** (cons nil nil)))
  91.       (cond ((null lst)
  92.          term)
  93.         ((one-way-unify term (cadr (car lst)) **unify-subst**)
  94.          (rewrite (apply-subst (car **unify-subst**) (caddr (car lst)))))
  95.         (t (rewrite-with-lemmas term (cdr lst))))))
  96.  
  97.   (defun boyer-setup ()
  98.     (add-lemma-lst
  99.      (quote ((equal (compile form)
  100.             (reverse (codegen (optimize form)
  101.                       (nil))))
  102.          (equal (eqp x y)
  103.             (equal (fix x)
  104.                (fix y)))
  105.          (equal (greaterp x y)
  106.             (lessp y x))
  107.          (equal (lesseqp x y)
  108.             (not (lessp y x)))
  109.          (equal (greatereqp x y)
  110.             (not (lessp x y)))
  111.          (equal (boolean x)
  112.             (or (equal x (t))
  113.             (equal x (f))))
  114.          (equal (iff x y)
  115.             (and (implies x y)
  116.              (implies y x)))
  117.          (equal (even1 x)
  118.             (if (zerop x)
  119.             (t)
  120.               (odd (- x 1))))
  121.          (equal (countps- l pred)
  122.             (countps-loop l pred (zero)))
  123.          (equal (fact- i)
  124.             (fact-loop i 1))
  125.          (equal (reverse- x)
  126.             (reverse-loop x (nil)))
  127.          (equal (divides x y)
  128.             (zerop (remainder y x)))
  129.          (equal (assume-true var alist)
  130.             (cons (cons var (t))
  131.               alist))
  132.          (equal (assume-false var alist)
  133.             (cons (cons var (f))
  134.               alist))
  135.          (equal (tautology-checker x)
  136.             (tautologyp (normalize x)
  137.                 (nil)))
  138.          (equal (falsify x)
  139.             (falsify1 (normalize x)
  140.                   (nil)))
  141.          (equal (prime x)
  142.             (and (not (zerop x))
  143.              (not (equal x (add1 (zero))))
  144.              (prime1 x (- x 1))))
  145.          (equal (and p q)
  146.             (if p (if q (t)
  147.                 (f))
  148.               (f)))
  149.          (equal (or p q)
  150.             (if p (t)
  151.               (if q (t)
  152.             (f))
  153.               (f)))
  154.          (equal (not p)
  155.             (if p (f)
  156.               (t)))
  157.          (equal (implies p q)
  158.             (if p (if q (t)
  159.                 (f))
  160.               (t)))
  161.          (equal (fix x)
  162.             (if (numberp x)
  163.             x
  164.               (zero)))
  165.          (equal (if (if a b c)
  166.             d e)
  167.             (if a (if b d e)
  168.               (if c d e)))
  169.          (equal (zerop x)
  170.             (or (equal x (zero))
  171.             (not (numberp x))))
  172.          (equal (plus (plus x y)
  173.               z)
  174.             (plus x (plus y z)))
  175.          (equal (equal (plus a b)
  176.                (zero))
  177.             (and (zerop a)
  178.              (zerop b)))
  179.          (equal (difference x x)
  180.             (zero))
  181.          (equal (equal (plus a b)
  182.                (plus a c))
  183.             (equal (fix b)
  184.                (fix c)))
  185.          (equal (equal (zero)
  186.                (difference x y))
  187.             (not (lessp y x)))
  188.          (equal (equal x (difference x y))
  189.             (and (numberp x)
  190.              (or (equal x (zero))
  191.                  (zerop y))))
  192.          (equal (meaning (plus-tree (append x y))
  193.                  a)
  194.             (plus (meaning (plus-tree x)
  195.                    a)
  196.               (meaning (plus-tree y)
  197.                    a)))
  198.          (equal (meaning (plus-tree (plus-fringe x))
  199.                  a)
  200.             (fix (meaning x a)))
  201.          (equal (append (append x y)
  202.                 z)
  203.             (append x (append y z)))
  204.          (equal (reverse (append a b))
  205.             (append (reverse b)
  206.                 (reverse a)))
  207.          (equal (times x (plus y z))
  208.             (plus (times x y)
  209.               (times x z)))
  210.          (equal (times (times x y)
  211.                z)
  212.             (times x (times y z)))
  213.          (equal (equal (times x y)
  214.                (zero))
  215.             (or (zerop x)
  216.             (zerop y)))
  217.          (equal (exec (append x y)
  218.               pds envrn)
  219.             (exec y (exec x pds envrn)
  220.               envrn))
  221.          (equal (mc-flatten x y)
  222.             (append (flatten x)
  223.                 y))
  224.          (equal (member x (append a b))
  225.             (or (member x a)
  226.             (member x b)))
  227.          (equal (member x (reverse y))
  228.             (member x y))
  229.          (equal (length (reverse x))
  230.             (length x))
  231.          (equal (member a (intersect b c))
  232.             (and (member a b)
  233.              (member a c)))
  234.          (equal (nth (zero)
  235.              i)
  236.             (zero))
  237.          (equal (exp i (plus j k))
  238.             (times (exp i j)
  239.                (exp i k)))
  240.          (equal (exp i (times j k))
  241.             (exp (exp i j)
  242.              k))
  243.          (equal (reverse-loop x y)
  244.             (append (reverse x)
  245.                 y))
  246.          (equal (reverse-loop x (nil))
  247.             (reverse x))
  248.          (equal (count-list z (sort-lp x y))
  249.             (plus (count-list z x)
  250.               (count-list z y)))
  251.          (equal (equal (append a b)
  252.                (append a c))
  253.             (equal b c))
  254.          (equal (plus (remainder x y)
  255.               (times y (quotient x y)))
  256.             (fix x))
  257.          (equal (power-eval (big-plus1 l i base)
  258.                 base)
  259.             (plus (power-eval l base)
  260.               i))
  261.          (equal (power-eval (big-plus x y i base)
  262.                 base)
  263.             (plus i (plus (power-eval x base)
  264.                   (power-eval y base))))
  265.          (equal (remainder y 1)
  266.             (zero))
  267.          (equal (lessp (remainder x y)
  268.                y)
  269.             (not (zerop y)))
  270.          (equal (remainder x x)
  271.             (zero))
  272.          (equal (lessp (quotient i j)
  273.                i)
  274.             (and (not (zerop i))
  275.              (or (zerop j)
  276.                  (not (equal j 1)))))
  277.          (equal (lessp (remainder x y)
  278.                x)
  279.             (and (not (zerop y))
  280.              (not (zerop x))
  281.              (not (lessp x y))))
  282.          (equal (power-eval (power-rep i base)
  283.                 base)
  284.             (fix i))
  285.          (equal (power-eval (big-plus (power-rep i base)
  286.                       (power-rep j base)
  287.                       (zero)
  288.                       base)
  289.                 base)
  290.             (plus i j))
  291.          (equal (gcd x y)
  292.             (gcd y x))
  293.          (equal (nth (append a b)
  294.              i)
  295.             (append (nth a i)
  296.                 (nth b (difference i (length a)))))
  297.          (equal (difference (plus x y)
  298.                 x)
  299.             (fix y))
  300.          (equal (difference (plus y x)
  301.                 x)
  302.             (fix y))
  303.          (equal (difference (plus x y)
  304.                 (plus x z))
  305.             (difference y z))
  306.          (equal (times x (difference c w))
  307.             (difference (times c x)
  308.                 (times w x)))
  309.          (equal (remainder (times x z)
  310.                    z)
  311.             (zero))
  312.          (equal (difference (plus b (plus a c))
  313.                 a)
  314.             (plus b c))
  315.          (equal (difference (add1 (plus y z))
  316.                 z)
  317.             (add1 y))
  318.          (equal (lessp (plus x y)
  319.                (plus x z))
  320.             (lessp y z))
  321.          (equal (lessp (times x z)
  322.                (times y z))
  323.             (and (not (zerop z))
  324.              (lessp x y)))
  325.          (equal (lessp y (plus x y))
  326.             (not (zerop x)))
  327.          (equal (gcd (times x z)
  328.              (times y z))
  329.             (times z (gcd x y)))
  330.          (equal (value (normalize x)
  331.                a)
  332.             (value x a))
  333.          (equal (equal (flatten x)
  334.                (cons y (nil)))
  335.             (and (nlistp x)
  336.              (equal x y)))
  337.          (equal (listp (gopher x))
  338.             (listp x))
  339.          (equal (samefringe x y)
  340.             (equal (flatten x)
  341.                (flatten y)))
  342.          (equal (equal (greatest-factor x y)
  343.                (zero))
  344.             (and (or (zerop y)
  345.                  (equal y 1))
  346.              (equal x (zero))))
  347.          (equal (equal (greatest-factor x y)
  348.                1)
  349.             (equal x 1))
  350.          (equal (numberp (greatest-factor x y))
  351.             (not (and (or (zerop y)
  352.                   (equal y 1))
  353.                   (not (numberp x)))))
  354.          (equal (times-list (append x y))
  355.             (times (times-list x)
  356.                (times-list y)))
  357.          (equal (prime-list (append x y))
  358.             (and (prime-list x)
  359.              (prime-list y)))
  360.          (equal (equal z (times w z))
  361.             (and (numberp z)
  362.              (or (equal z (zero))
  363.                  (equal w 1))))
  364.          (equal (greatereqpr x y)
  365.             (not (lessp x y)))
  366.          (equal (equal x (times x y))
  367.             (or (equal x (zero))
  368.             (and (numberp x)
  369.                  (equal y 1))))
  370.          (equal (remainder (times y x)
  371.                    y)
  372.             (zero))
  373.          (equal (equal (times a b)
  374.                1)
  375.             (and (not (equal a (zero)))
  376.              (not (equal b (zero)))
  377.              (numberp a)
  378.              (numberp b)
  379.              (equal (- a 1)
  380.                 (zero))
  381.              (equal (- b 1)
  382.                 (zero))))
  383.          (equal (lessp (length (delete x l))
  384.                (length l))
  385.             (member x l))
  386.          (equal (sort2 (delete x l))
  387.             (delete x (sort2 l)))
  388.          (equal (dsort x)
  389.             (sort2 x))
  390.          (equal (length (cons x1
  391.                   (cons x2
  392.                     (cons x3 (cons x4
  393.                                (cons x5
  394.                                  (cons x6 x7)))))))
  395.             (plus 6 (length x7)))
  396.          (equal (difference (add1 (add1 x))
  397.                 2)
  398.             (fix x))
  399.          (equal (quotient (plus x (plus x y))
  400.                   2)
  401.             (plus x (quotient y 2)))
  402.          (equal (sigma (zero)
  403.                i)
  404.             (quotient (times i (add1 i))
  405.                   2))
  406.          (equal (plus x (add1 y))
  407.             (if (numberp y)
  408.             (add1 (plus x y))
  409.               (add1 x)))
  410.          (equal (equal (difference x y)
  411.                (difference z y))
  412.             (if (lessp x y)
  413.             (not (lessp y z))
  414.               (if (lessp z y)
  415.               (not (lessp y x))
  416.             (equal (fix x)
  417.                    (fix z)))))
  418.          (equal (meaning (plus-tree (delete x y))
  419.                  a)
  420.             (if (member x y)
  421.             (difference (meaning (plus-tree y)
  422.                          a)
  423.                     (meaning x a))
  424.               (meaning (plus-tree y)
  425.                    a)))
  426.          (equal (times x (add1 y))
  427.             (if (numberp y)
  428.             (plus x (times x y))
  429.               (fix x)))
  430.          (equal (nth (nil)
  431.              i)
  432.             (if (zerop i)
  433.             (nil)
  434.               (zero)))
  435.          (equal (last (append a b))
  436.             (if (listp b)
  437.             (last b)
  438.               (if (listp a)
  439.               (cons (car (last a))
  440.                 b)
  441.             b)))
  442.          (equal (equal (lessp x y)
  443.                z)
  444.             (if (lessp x y)
  445.             (equal t z)
  446.               (equal f z)))
  447.          (equal (assignment x (append a b))
  448.             (if (assignedp x a)
  449.             (assignment x a)
  450.               (assignment x b)))
  451.          (equal (car (gopher x))
  452.             (if (listp x)
  453.             (car (flatten x))
  454.               (zero)))
  455.          (equal (flatten (cdr (gopher x)))
  456.             (if (listp x)
  457.             (cdr (flatten x))
  458.               (cons (zero)
  459.                 (nil))))
  460.          (equal (quotient (times y x)
  461.                   y)
  462.             (if (zerop y)
  463.             (zero)
  464.               (fix x)))
  465.          (equal (get j (set i val mem))
  466.             (if (eqp j i)
  467.             val
  468.               (get j mem)))))))
  469.  
  470.   (defun tautologyp (x true-lst false-lst)
  471.     (cond ((truep x true-lst)
  472.        t)
  473.       ((falsep x false-lst)
  474.        nil)
  475.       ((atom x)
  476.        nil)
  477.       ((eq (car x)
  478.            (quote if))
  479.        (cond ((truep (cadr x)
  480.              true-lst)
  481.           (tautologyp (caddr x)
  482.                   true-lst false-lst))
  483.          ((falsep (cadr x)
  484.               false-lst)
  485.           (tautologyp (cadddr x)
  486.                   true-lst false-lst))
  487.          (t (and (tautologyp (caddr x)
  488.                      (cons (cadr x)
  489.                        true-lst)
  490.                      false-lst)
  491.              (tautologyp (cadddr x)
  492.                      true-lst
  493.                      (cons (cadr x)
  494.                         false-lst))))))
  495.       (t nil)))
  496.  
  497.   (defun tautp (x)
  498.     (tautologyp (rewrite x)
  499.         nil nil))
  500.  
  501.   (defun boyer-test ()
  502.     (prog (ans term)
  503.       (setq term
  504.         (apply-subst
  505.          (quote ((x f (plus (plus a b)
  506.                     (plus c (zero))))
  507.              (y f (times (times a b)
  508.                      (plus c d)))
  509.              (z f (reverse (append (append a b)
  510.                            (nil))))
  511.              (u equal (plus a b)
  512.                 (difference x y))
  513.              (w lessp (remainder a b)
  514.                 (member a (length b)))))
  515.          (quote (implies (and (implies x y)
  516.                       (and (implies y z)
  517.                        (and (implies z u)
  518.                         (implies u w))))
  519.                  (implies x w)))))
  520.       (setq ans (tautp term))))
  521.  
  522. (defun boyer-short-test ()
  523.   (prog (ans term)
  524.         (setq term
  525.               (apply-subst
  526.                 (quote ((x f (plus (plus a b)
  527.                                    (plus c (zero))))
  528.                         (y f (times (times a b)
  529.                                     (plus c d)))
  530.                         (z f (reverse (append (append a b)
  531.                                               (nil))))
  532.                         (u equal (plus a b)
  533.                            (difference x y))
  534.                         (w lessp (remainder a b)
  535.                            (member a (length b)))))
  536.                 (quote (implies (and (implies x y)
  537.                                      (and (implies z u)
  538.                                           (implies u w)))
  539.                                 (implies x w)))))
  540.         (setq ans (tautp term))))
  541.  
  542. (defun boyer-very-short-test ()
  543.   (prog (ans term)
  544.         (setq term
  545.               (apply-subst
  546.                 (quote ((x f (plus (plus a b)
  547.                                    (plus c (zero))))
  548.                         (y f (times (times a b)
  549.                                     (plus c d)))
  550.                         (z f (reverse (append (append a b)
  551.                                               (nil))))
  552.                         (u equal (plus a b)
  553.                            (difference x y))
  554.                         (w lessp (remainder a b)
  555.                            (member a (length b)))))
  556.                 (quote (implies x y))))
  557.         (setq ans (tautp term))))
  558.  
  559.   (defun trans-of-implies (n)
  560.     (list (quote implies)
  561.       (trans-of-implies1 n)
  562. xxv      (list (quote implies)
  563.         0 n)))
  564.  
  565.   (defun trans-of-implies1 (n)
  566.     (cond ((eql n 1)
  567.        (list (quote implies)        
  568.          0 1))
  569.       (t (list (quote and)
  570.            (list (quote implies)
  571.              (- n 1)
  572.              n)
  573.            (trans-of-implies1 (- n 1))))))
  574.  
  575.  
  576.   (defun truep (x lst)
  577.     (or (equal x (quote (t)))
  578.     (member x lst eq)))
  579.  
  580.   (boyer-setup)
  581.   (defvar setup-performed-p t)
  582.  
  583.   (defun testboyer ()
  584.     (print (boyer-test)))
  585.  
  586.   (defun testshortboyer ()
  587.     (print (boyer-short-test)))
  588.  
  589.   (defun testveryshortboyer ()
  590.     (print (boyer-very-short-test)))
  591.  
  592.   )                    ; end of module
  593.